es:ES, ff:FIFO, f2f+:F2F+-decls, sndr, rcvr:ff.C, e, e':E. f2f+-event(e)   

latex

Definitions	t.2, t.1, P  Q, P & Q, is_ack , is_req  , P  Q, f2f+-event(e), , t  T, F2F+-decls, FIFO, x:A. B(x)
Lemmas	event system wf, fifo wf, es-state wf, top wf, not wf, fifoS wf, decidable wf, es-loc wf, fifoR wf, bool wf, es-dtype wf, Id wf, fifoC wf, es-E wf, rcv-it wf, snd-it wf